\begin{table}[!t]
\centering
\fontsize{9}{11}\selectfont
\begin{tabular*}{\linewidth}{@{\extracolsep{\fill}}cllllll}\\\hlx{hv}
\multirow{2}{*}{\# Args} & \multicolumn{3}{c}{D\&Q Enumeration} & \multicolumn{3}{c}{CVC4}\\\hlx{vc{2-4,5-7}v}
& Size & Time (s) & \# Comp. & Size & Time (s) & \# Comp\\\hlx{h}
2 & 6 & $< 0.1$ & 1 & 6 & $< 0.1$ & 1\\
3 & 16 & 0.16 & 3 & 25 & $< 0.1$ & 4\\
4 & 36 & 0.77 & 7 & 55 & $< 0.1$ & 9\\
5 & 76 & 6.2 & 15 & 96 & $< 0.1$ & 16\\
6 & 156 & 63.2 & 31 & 148 & $< 0.1$ & 25\\
7 & 316 & 546 & 63 & 211 & $< 0.1$ & 36\\
8 & -- & TO & -- & 285 & $< 0.1$ & 49\\
9 & -- & TO & -- & 370 & 0.1 & 64\\
10 & -- & TO & -- & 466 & 0.15 & 81\\\hlx{hv}
\end{tabular*}
\vspace*{1mm}
\caption{Results on the parameterized ``max'' benchmarks.}
\label{table:max_results}
\end{table}
